(set-info :source |fuzzsmt|)
(set-info :smt-lib-version 2.0)
(set-info :category "random")
(set-info :status unknown)
(set-logic QF_LRA)
(declare-fun v0 () Real)
(assert (let ((e1 1))
(let ((e2 0))
(let ((e3 1))
(let ((e4 (+ v0 v0)))
(let ((e5 (- v0 e4)))
(let ((e6 (- e5 v0)))
(let ((e7 (* e2 v0)))
(let ((e8 (/ e2 (- e3))))
(let ((e9 (* e7 (- e3))))
(let ((e10 (/ e1 e1)))
(let ((e11 (distinct e10 e6)))
(let ((e12 (<= e10 e6)))
(let ((e13 (<= v0 e8)))
(let ((e14 (> e9 e10)))
(let ((e15 (= e5 e4)))
(let ((e16 (>= e4 e7)))
(let ((e17 (ite e15 e6 e6)))
(let ((e18 (ite e16 e5 e8)))
(let ((e19 (ite e13 e9 e9)))
(let ((e20 (ite e11 e7 v0)))
(let ((e21 (ite e14 e7 e10)))
(let ((e22 (ite e12 e4 e9)))
(let ((e23 (>= e6 e17)))
(let ((e24 (<= e9 e5)))
(let ((e25 (> v0 e19)))
(let ((e26 (distinct e6 e10)))
(let ((e27 (= e10 e7)))
(let ((e28 (distinct e9 e8)))
(let ((e29 (= e6 e22)))
(let ((e30 (>= e4 v0)))
(let ((e31 (< v0 e9)))
(let ((e32 (= e8 e6)))
(let ((e33 (< e4 e9)))
(let ((e34 (> e19 e22)))
(let ((e35 (> e21 e10)))
(let ((e36 (< e5 e21)))
(let ((e37 (< v0 e22)))
(let ((e38 (> e21 e7)))
(let ((e39 (<= e20 e20)))
(let ((e40 (= e18 e20)))
(let ((e41 (ite e27 e37 e35)))
(let ((e42 (xor e29 e26)))
(let ((e43 (ite e38 e25 e42)))
(let ((e44 (or e12 e33)))
(let ((e45 (not e13)))
(let ((e46 (ite e36 e24 e28)))
(let ((e47 (or e15 e16)))
(let ((e48 (= e45 e43)))
(let ((e49 (not e32)))
(let ((e50 (and e40 e34)))
(let ((e51 (=> e44 e48)))
(let ((e52 (and e11 e50)))
(let ((e53 (or e46 e41)))
(let ((e54 (ite e47 e47 e30)))
(let ((e55 (=> e54 e31)))
(let ((e56 (= e39 e51)))
(let ((e57 (not e56)))
(let ((e58 (= e49 e53)))
(let ((e59 (and e23 e52)))
(let ((e60 (not e58)))
(let ((e61 (ite e59 e60 e57)))
(let ((e62 (=> e61 e55)))
(let ((e63 (= e14 e62)))
e63
))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))

(check-sat)
